A:Type, B, C:(AType), eq:EqDecider(A), f:a:A fp B(a), g:a:A fp C(a).
(x:A. x  dom(f)  x  dom(g)  B(x)  C(x))  f || g  Prop 

latex

Definitions	f || g, Prop, f(x), P & Q, b, x  dom(f), Top, a:A fp B(a), x. t(x), x(s), EqDecider(T), t  T, x:A. B(x), P  Q
Lemmas	deq wf, fpf wf, fpf-trivial-subtype-top, fpf-dom wf, assert wf, fpf-ap wf